\begin{tabbing}
$\forall$\=${\it ds}$:(Id$\rightarrow$Type), ${\it da}$:(Id$\rightarrow$Knd$\rightarrow$Type), $A$, $B$:Type, $X$:Interface(${\it ds}$;${\it da}$;$A$), $Y$:Interface(${\it ds}$;${\it da}$;$B$),\+
\\[0ex]${\it es}$:ES.
\-\\[0ex]es{-}decl(${\it es}$;${\it ds}$;${\it da}$)
\\[0ex]$\Rightarrow$ [[$X$]] $\cap$ [[$Y$]] = 0
\\[0ex]$\Rightarrow$ (es{-}interface{-}right([[interface{-}union($X$;$Y$)]]) = [[$Y$]] $\in$ AbsInterface($B$))
\end{tabbing}